update-antecedent{i:l}(es;Cmd;Sys;Config;u)
== (e:{e:E(Sys)| csupdate?(Sys(e))} . (u(e) < e))
== & (e:{e:E(Sys)| csupdate?(Sys(e))} .
== & (((((u(e))  Sys))
== & (( (valid-sys(es;Config;Sys;u(e)) & csupdate-cmds(Sys(e)) = sys-cmds(Sys(u(e)))))
== & (& ((((u(e))  Config))
== & (& ( ((ccsucc?(Config(u(e))))
== & (& ( & ccsucc-id(Config(u(e))) = loc(e)
== & (& ( & let n = ccsucc-num(Config(u(e))) in
== & (& ( & let n(n < ||cmd-history(u(e))||) & csupdate-cmds(Sys(e)) = nth_tl(n;cmd-history(u(e))))))
== & (e1, e2:{e:E(Sys)| csupdate?(Sys(e))} .
== & ((u(e1) <loc u(e2))  (loc(e1) = loc(e2))  (e1 <loc e2))
== & (e:{e:E(Sys)| csupdate?(Sys(e))} , s:E.
== & ((s <loc u(e))
== & ( ((((s  Sys)) & valid-sys(es;Config;Sys;s))  (((s  Config)) & (ccsucc?(Config(s)))))
== & ( (e':{e:E(Sys)| csupdate?(Sys(e))} . (u(e') = s))) 

latex

---

clarification:

update-antecedent{i:l}
update-antecedent(es; Cmd; Sys; Config; u)
== (e:{e:es-E-interface(es;Sys)| csupdate?(Sys(e))} . es-causl(es; (u(e)); e))
== & (e:{e:es-E-interface(es;Sys)| csupdate?(Sys(e))} .
== & (((((u(e))  Sys))
== & (( (valid-sys(es;Config;Sys;u(e))
== & (( & csupdate-cmds(Sys(e)) = sys-cmds(Sys(u(e)))  (Cmd List)))
== & (& ((((u(e))  Config))
== & (& ( ((ccsucc?(Config(u(e))))
== & (& ( & ccsucc-id(Config(u(e))) = es-loc(es; e)  Id
== & (& ( & let n = ccsucc-num(Config(u(e))) in
== & (& ( & let n(n < ||cmd-history{i:l}
== & (& ( & let n(n < ||cmd-history(es; Config; Cmd; Sys; (u(e)))||)
== & (& ( & let & csupdate-cmds(Sys(e))
== & (& ( & let & =
== & (& ( & let & nth_tl(n;cmd-history{i:l}(es; Config; Cmd; Sys; (u(e))))
== & (& ( & let &  (Cmd List))))
== & (e1:{e:es-E-interface(es;Sys)| csupdate?(Sys(e))} ,
== & (e2:{e:es-E-interface(es;Sys)| csupdate?(Sys(e))} .
== & (es-locl(es; (u(e1)); (u(e2)))
== & ( (es-loc(es; e1) = es-loc(es; e2)  Id)
== & ( es-locl(es; e1; e2))
== & (e:{e:es-E-interface(es;Sys)| csupdate?(Sys(e))} , s:es-E(es).
== & (es-locl(es; s; (u(e)))
== & ( ((((s  Sys)) & valid-sys(es;Config;Sys;s))  (((s  Config)) & (ccsucc?(Config(s)))))
== & ( (e':{e:es-E-interface(es;Sys)| csupdate?(Sys(e))} . (u(e') = s  es-E(es)))) 

latex

Definitions	(e < e'), sys-cmds(x), ccsucc-id(x), let x = a in b(x), ccsucc-num(x), a < b, ||as||, type List, csupdate-cmds(x), nth_tl(n;as), cmd-history(e), Id, loc(e), x:A. B(x), (e <loc e'), P  Q, P  Q, valid-sys(es;Config;Sys;e), P & Q, e  X, ccsucc?(x), x:A. B(x), {x:A| B(x)} , E(X), b, csupdate?(x), X(e), s = t, E, f(a)
FDL editor aliases	update-antecedent